Many applications of formal methods rely on generating formulae of first order logic and proving or disproving their satisfiability with respect to some background theory, which is often obtained as a combination of several theories. In the literature, this kind of satisfiability problem is called Satisfiability Modulo Theories (SMT). In this thesis, we focus on the design of decision procedures for SMT problems by integrating saturation techniques based on rewriting for finitely axiomatized theories, together with combination techniques for unions of theories. The first contribution of the thesis is a rational reconstruction of the combination methods proposed by Nelson-Oppen, Shostak and others in an uniform framework. This is the starting point for further investigations. We then introduce the concept of extended canonizer and derive a modularity result for a new class of theories. This is in contrast with the lack of modularity of the class of theories considered by the Shostak method. The second contribution concerns the problem of combining rewriting-based satisfiability procedures using the Nelson-Oppen method. We use meta-saturation to develop automatic proof techniques to check important requirements for the combinability of such procedures. When meta-saturation halts for a theory, its output allows us to reason about the combinability of a rewriting-based satisfiability procedure for this theory. The third contribution of this thesis is about the integration of decision procedures into SMT solvers. We consider the problem of augmenting decision procedures with the capability of computing conflict sets without degrading performances, as well as the problem of modularly constructing conflict sets for a combined theory. In this respect, we extend the Nelson-Oppen combination method to modularly build conflict sets for disjoint unions of theories. We also study how the computed conflict sets relate to an appropriate notion of minimality.

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004994 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004994 | SxmlIndent | more

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Hal:tel-00580582
   |texte=   Conception de Procédures de Décision par Combinaison et Saturation
}}